|
In computing, compiler correctness is the branch of software engineering that deals with trying to show that a compiler behaves according to its language specification. Techniques include developing the compiler using formal methods and using rigorous testing (often called compiler validation) on an existing compiler. ==Formal methods== Compiler validation with formal methods involves a long chain of formal, deductive logic. However, since the tool to find the proof (theorem prover) is implemented in software and is complex, there is a high probability it will contain errors. One approach has been to use a tool that verifies the proof (a proof checker) which because it is much simpler than a proof-finder is less likely to contain errors. A language described as a subset of C has been formally verified (although no proof was given of its connection to the C Standard), and the proof has been machine checked. Methods include model checking, formal verification, and provably correct semantics-directed compiler generation.〔Stephan Diehl, ''Natural Semantics Directed Generation of Compilers and Abstract Machines'',Formal Aspects of Computing, Vol. 12 (2), Springer Verlag, 2000. 〕 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Compiler correctness」の詳細全文を読む スポンサード リンク
|